Propositional proof systems and bounded arithmetic for logspace and nondeterministic logspace

Abstract: We discuss logics for proof systems that correspond to deterministic logspace computation and to nondeterministic logspace computation. The first component is propositional proof systems in which lines are either decision diagrams, represented as decision trees with extension variables, or nondeterministic decision diagrams, represented by decision trees with nondeterministic choices and extension variables. The second component is the bounded arithmetic theories VL and VNL. This is part of a program of developing logics for weak classes of computational complexity. A highlight of this kind of work is tight relationships between propositional proof systems, (second-order) theories of bounded arithmetic, and computational complexity. Our results are in part revamped versions of prior theories for logspace and nondeterministic logspace due to Zambella, Cook, Nguyen, and Perron. The talk will survey past results, and report on joint work-in-progress with Anupam Das and Alexander Knop.

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/